Formal Specification
--------------------

<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.

SPDX-License-Identifier: CC0-1.0
-->

[(Up)](../../README.md#topics) | _See also: [Software Engineering](../Software%20Engineering/README.md#software-engineering), [Logic](../Logic/README.md#logic), [Refinement Calculus](../Refinement%20Calculus/README.md#refinement-calculus), [Model Checking](../Model%20Checking/README.md#model-checking), [Theorem Proving](../Theorem%20Proving/README.md#theorem-proving), [TLA(plus)](../TLA(plus)/README.md#tlaplus)_

- - - -


### Web resources

[Notes on B. Meyer\'s \"On Formalism in Specifications\"](https://www.cs.scranton.edu/~mccloske/courses/se507/meyer_formalism_in_specs_lec.html) ★

[Bertrand Meyer's technology+ blog - Software engineering, programming methodology, languages, verification, general technology, publication culture, and more](https://bertrandmeyer.com/) ★

[Attempto Controlled English - Wikipedia](https://en.wikipedia.org/wiki/Attempto_Controlled_English)

[Attempto Project](http://attempto.ifi.uzh.ch/site/) ★★ [💭](commentary/Chris%20Pressey.md#attempto-project)

[About the Unified Modeling Language Specification Version 2.5.1](https://www.omg.org/spec/UML/2.5.1) ★

[Systems modeling language - Wikipedia](https://en.wikipedia.org/wiki/Systems_modeling_language)

[SysML Open Source Project: What is SysML? Who created it?](https://sysml.org/index.html) ★

[SE 507 Algebraic Specifications](https://www.cs.scranton.edu/~mccloske/courses/se507/alg_specs_lec.html) ★★★

[Developing an Iterative Program to Compute a Tail Recursive Function](https://www.cs.scranton.edu/~mccloske/courses/se504/tail_recursion.html) ★

[Software Blueprints Web Pages](https://www.dai.ed.ac.uk/groups/ssp/bookpages/blueprints.html)


### Papers

[The role of formalism in system requirements (full version)](https://arxiv.org/abs/1911.02564) ★★★

[Consistency Checking of Functional Requirements](https://arxiv.org/abs/1804.10486)

[Consistency Checking in Requirements Analysis](https://jar-ben.github.io/papers/ISSTA2017.pdf)

[Automated Consistency Checking of Requirements Specifications](https://apps.dtic.mil/sti/tr/pdf/ADA465574.pdf)

[Automatic program generation from specifications using PROLOG](https://archive.org/details/nasa_techdoc_19880014812) ★

Syntactic Theories in Practice (online @ [tidsskrift.dk](https://tidsskrift.dk/brics/article/view/21721)) ★ [💭](commentary/Chris%20Pressey.md#syntactic-theories-in-practice)

_(in [Philosophy](../Philosophy/README.md#philosophy))_ [Tossing Algebraic Flowers down the Great Divide](https://cseweb.ucsd.edu/~goguen/pps/tcs97.pdf) ★★★

_(in [Type Systems](../Type%20Systems/README.md#type-systems))_ Should Your Specification Language Be Typed? (online @ [lamport.azurewebsites.net](http://lamport.azurewebsites.net/pubs/lamport-types.pdf)) ★★★ [💭](commentary/Chris%20Pressey.md#should-your-specification-language-be-typed)


### Books

Algebraic Specification (borrow @ [archive.org](https://archive.org/details/algebraicspecifi0000unse)) ★ [💭](commentary/Chris%20Pressey.md#algebraic-specification)

Language Prototyping: an Algebraic Specification Approach (borrow @ [archive.org](https://archive.org/details/languageprototyp0000unse)) ★ [💭](commentary/Chris%20Pressey.md#language-prototyping-an-algebraic-specification-approach)

The Essence of Z (borrow @ [archive.org](https://archive.org/details/essenceofz0000curr)) ★ [💭](commentary/Chris%20Pressey.md#the-essence-of-z)

Introduction to Z and Discrete Methods (borrow @ [archive.org](https://archive.org/details/introductiontodi0000ince)) ★ [💭](commentary/Chris%20Pressey.md#introduction-to-z-and-discrete-methods)

Understanding Z (borrow @ [archive.org](https://archive.org/details/understandingzsp0000spiv)) [💭](commentary/Chris%20Pressey.md#understanding-z)

Program specification and transformation (borrow @ [archive.org](https://archive.org/details/programspecifica0000ifip)) ★ [💭](commentary/Chris%20Pressey.md#program-specification-and-transformation)

Semantics, applications, and implementation of program generation (online @ [archive.org](https://archive.org/details/springer_10.1007-3-540-44806-3)) ★ [💭](commentary/Chris%20Pressey.md#semantics-applications-and-implementation-of-program-generation)